<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>10. Linear algebra &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script src="_static/jquery.js?v=5d32c60e"></script>
        <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
        <script src="_static/documentation_options.js?v=7048e04d"></script>
        <script src="_static/doctools.js?v=9a2dae69"></script>
        <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="11. Topology" href="C11_Topology.html" />
    <link rel="prev" title="9. Groups and Rings" href="C09_Groups_and_Rings.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">10. Linear algebra</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#vector-spaces-and-linear-maps">10.1. Vector spaces and linear maps</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#vector-spaces">10.1.1. Vector spaces</a></li>
<li class="toctree-l3"><a class="reference internal" href="#linear-maps">10.1.2. Linear maps</a></li>
<li class="toctree-l3"><a class="reference internal" href="#sums-and-products-of-vector-spaces">10.1.3. Sums and products of vector spaces</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#subspaces-and-quotients">10.2. Subspaces and quotients</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#subspaces">10.2.1. Subspaces</a></li>
<li class="toctree-l3"><a class="reference internal" href="#complete-lattice-structure-and-internal-direct-sums">10.2.2. Complete lattice structure and internal direct sums</a></li>
<li class="toctree-l3"><a class="reference internal" href="#subspace-spanned-by-a-set">10.2.3. Subspace spanned by a set</a></li>
<li class="toctree-l3"><a class="reference internal" href="#pushing-and-pulling-subspaces">10.2.4. Pushing and pulling subspaces</a></li>
<li class="toctree-l3"><a class="reference internal" href="#quotient-spaces">10.2.5. Quotient spaces</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#endomorphisms">10.3. Endomorphisms</a></li>
<li class="toctree-l2"><a class="reference internal" href="#matrices-bases-and-dimension">10.4. Matrices, bases and dimension</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#matrices">10.4.1. Matrices</a></li>
<li class="toctree-l3"><a class="reference internal" href="#bases">10.4.2. Bases</a></li>
<li class="toctree-l3"><a class="reference internal" href="#dimension">10.4.3. Dimension</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">10. </span>Linear algebra</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C10_Linear_Algebra.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="linear-algebra">
<span id="id1"></span><h1><span class="section-number">10. </span>Linear algebra<a class="headerlink" href="#linear-algebra" title="Link to this heading">&#61633;</a></h1>
<section id="vector-spaces-and-linear-maps">
<h2><span class="section-number">10.1. </span>Vector spaces and linear maps<a class="headerlink" href="#vector-spaces-and-linear-maps" title="Link to this heading">&#61633;</a></h2>
<section id="vector-spaces">
<h3><span class="section-number">10.1.1. </span>Vector spaces<a class="headerlink" href="#vector-spaces" title="Link to this heading">&#61633;</a></h3>
<p id="index-0">We will start directly abstract linear algebra, taking place in a vector space over any field.
However you can find information about matrices in
<a class="reference internal" href="#matrices"><span class="std std-numref">Section 10.4.1</span></a> which does not logically depend on this abstract theory.
Mathlib actually deals with a more general version of linear algebra involving the word module,
but for now we will pretend this is only an eccentric spelling habit.</p>
<p>The way to say &#8220;let <span class="math notranslate nohighlight">\(K\)</span> be a field and let <span class="math notranslate nohighlight">\(V\)</span> be a vector space over <span class="math notranslate nohighlight">\(K\)</span>&#8221;
(and make them implicit arguments to later results) is:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Field</span><span class="w"> </span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span>
</pre></div>
</div>
<p>We explained in <a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 8</span></a> why we need two separate
typeclasses <code class="docutils literal notranslate"><span class="pre">[AddCommGroup</span> <span class="pre">V]</span> <span class="pre">[Module</span> <span class="pre">K</span> <span class="pre">V]</span></code>.
The short version is the following.
Mathematically we want to say that having a <span class="math notranslate nohighlight">\(K\)</span>-vector space structure
implies having an additive commutative group structure.
We could tell this to Lean. But then whenever Lean would need to find such a
group structure on a type <span class="math notranslate nohighlight">\(V\)</span>, it would go hunting for vector space
structures using a <em>completely unspecified</em> field <span class="math notranslate nohighlight">\(K\)</span> that cannot be inferred
from <span class="math notranslate nohighlight">\(V\)</span>.
This would be very bad for the type class synthesis system.</p>
<p>The multiplication of a vector <cite>v</cite> by a scalar <cite>a</cite> is denoted by
<cite>a &#8226; v</cite>. We list a couple of algebraic rules about the interaction of this
operation with addition in the following examples. Of course <cite>simp</cite> or <cite>apply?</cite>
would find those proofs. There is also a <cite>module</cite> tactic that solves goals
following from the axioms of vector spaces and fields, in the same way the
<cite>ring</cite> tactic is used in commutative rings or the <cite>group</cite> tactic is used in
groups. But it is still useful to remember that scalar
multiplication is abbreviated <cite>smul</cite> in lemma names.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">u</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="o">(</span><span class="n">u</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">smul_add</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">v</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">u</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">add_smul</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">u</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">u</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">smul_comm</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">u</span>
</pre></div>
</div>
<p>As a quick note for more advanced readers, let us point out that, as suggested by
terminology, Mathlib&#8217;s linear algebra also covers modules over (not necessarily commutative)
rings.
In fact it even covers semi-modules over semi-rings. If you think you do not need
this level of generality, you can meditate the following example that nicely captures
a lot of algebraic rules about ideals acting on submodules:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommSemiring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommMonoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Module</span><span class="w"> </span><span class="o">(</span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">Submodule</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">inferInstance</span>
</pre></div>
</div>
</section>
<section id="linear-maps">
<h3><span class="section-number">10.1.2. </span>Linear maps<a class="headerlink" href="#linear-maps" title="Link to this heading">&#61633;</a></h3>
<p id="index-1">Next we need linear maps. Like group morphisms, linear maps in Mathlib are bundled maps, i.e. packages
made of a map and proofs of its linearity properties.
Those bundled maps are converted to ordinary functions when applied.
See <a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 8</span></a> for more information about this design.</p>
<p>The type of linear maps between two <code class="docutils literal notranslate"><span class="pre">K</span></code>-vector spaces
<code class="docutils literal notranslate"><span class="pre">V</span></code> and <code class="docutils literal notranslate"><span class="pre">W</span></code> is denoted by <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">W</span></code>. The subscript <cite>l</cite> stands for linear.
At first it may feel odd to specify <code class="docutils literal notranslate"><span class="pre">K</span></code> in this notation.
But this is crucial when several fields come into play.
For instance real-linear maps from <span class="math notranslate nohighlight">\(&#8450;\)</span> to <span class="math notranslate nohighlight">\(&#8450;\)</span> are every map <span class="math notranslate nohighlight">\(z &#8614; az + b\bar{z}\)</span>
while only the maps <span class="math notranslate nohighlight">\(z &#8614; az\)</span> are complex linear, and this difference is crucial in
complex analysis.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">W</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">]</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">map_smul</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">v</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="n">w</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">w</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">w</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">map_add</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">w</span>
</pre></div>
</div>
<p>Note that <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">W</span></code> itself carries interesting algebraic structures (this
is part of the motivation for bundling those maps).
It is a <code class="docutils literal notranslate"><span class="pre">K</span></code>-vector space so we can add linear maps and multiply them by scalars.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>
</pre></div>
</div>
<p>One downside of using bundled maps is that we cannot use ordinary function composition.
We need to use <code class="docutils literal notranslate"><span class="pre">LinearMap.comp</span></code> or the notation <code class="docutils literal notranslate"><span class="pre">&#8728;&#8343;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">&#952;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;.comp</span><span class="w"> </span><span class="n">&#952;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">&#952;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>
</pre></div>
</div>
<p>There are two main ways to construct linear maps.
First we can build the structure by providing the function and the linearity proof.
As usual, this is facilitated by the structure code action: you can type
<code class="docutils literal notranslate"><span class="pre">example</span> <span class="pre">:</span> <span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">V</span> <span class="pre">:=</span> <span class="pre">_</span></code> and use the code action &#8220;Generate a skeleton&#8221; attached to the
underscore.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">toFun</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">v</span>
<span class="w">  </span><span class="n">map_add&#39;</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">smul_add</span><span class="w"> </span><span class="bp">..</span>
<span class="w">  </span><span class="n">map_smul&#39;</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">smul_comm</span><span class="w"> </span><span class="bp">..</span>
</pre></div>
</div>
<p>You may wonder why the proof fields of <code class="docutils literal notranslate"><span class="pre">LinearMap</span></code> have names ending with a prime.
This is because they are defined before the coercion to functions is defined, hence they are
phrased in terms of <code class="docutils literal notranslate"><span class="pre">LinearMap.toFun</span></code>. Then they are restated as <code class="docutils literal notranslate"><span class="pre">LinearMap.map_add</span></code>
and <code class="docutils literal notranslate"><span class="pre">LinearMap.map_smul</span></code> in terms of the coercion to function.
This is not yet the end of the story. One also wants a version of <code class="docutils literal notranslate"><span class="pre">map_add</span></code> that applies to
any (bundled) map preserving addition, such as additive group morphisms, linear maps, continuous
linear maps, <code class="docutils literal notranslate"><span class="pre">K</span></code>-algebra maps etc&#8230; This one is <code class="docutils literal notranslate"><span class="pre">map_add</span></code> (in the root namespace).
The intermediate version, <code class="docutils literal notranslate"><span class="pre">LinearMap.map_add</span></code> is a bit redundant but allows to use dot notation, which
can be nice sometimes. A similar story exists for <code class="docutils literal notranslate"><span class="pre">map_smul</span></code>, and the general framework
is explained in <a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 8</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;.map_add&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">,</span><span class="w"> </span><span class="n">&#966;.toFun</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;.toFun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">&#966;.toFun</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;.map_add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">,</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">map_add</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">,</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
</pre></div>
</div>
<p>One can also build linear maps from the ones that are already defined in Mathlib
using various combinators.
For instance the above example is already known as <code class="docutils literal notranslate"><span class="pre">LinearMap.lsmul</span> <span class="pre">K</span> <span class="pre">V</span> <span class="pre">3</span></code>.
There are several reason why <code class="docutils literal notranslate"><span class="pre">K</span></code> and <code class="docutils literal notranslate"><span class="pre">V</span></code> are explicit arguments here.
The most pressing one is that from a bare <code class="docutils literal notranslate"><span class="pre">LinearMap.lsmul</span> <span class="pre">3</span></code> there would be no way
for Lean to infer <code class="docutils literal notranslate"><span class="pre">V</span></code> or even <code class="docutils literal notranslate"><span class="pre">K</span></code>.
But also <code class="docutils literal notranslate"><span class="pre">LinearMap.lsmul</span> <span class="pre">K</span> <span class="pre">V</span></code> is an interesting object by itself: it has type
<code class="docutils literal notranslate"><span class="pre">K</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">V</span></code>, meaning it is a <code class="docutils literal notranslate"><span class="pre">K</span></code>-linear map from <code class="docutils literal notranslate"><span class="pre">K</span></code>
&#8212;seen as a vector space over itself&#8212; to the space of <code class="docutils literal notranslate"><span class="pre">K</span></code>-linear maps from <code class="docutils literal notranslate"><span class="pre">V</span></code> to <code class="docutils literal notranslate"><span class="pre">V</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">LinearMap.lsmul</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">LinearMap.lsmul</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
</pre></div>
</div>
<p>There is also a type <code class="docutils literal notranslate"><span class="pre">LinearEquiv</span></code> of linear isomorphisms denoted by <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8771;&#8343;[K]</span> <span class="pre">W</span></code>.
The inverse of <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">V</span> <span class="pre">&#8771;&#8343;[K]</span> <span class="pre">W</span></code> is <code class="docutils literal notranslate"><span class="pre">f.symm</span> <span class="pre">:</span> <span class="pre">W</span> <span class="pre">&#8771;&#8343;[K]</span> <span class="pre">V</span></code>,
composition of <code class="docutils literal notranslate"><span class="pre">f</span></code> and <code class="docutils literal notranslate"><span class="pre">g</span></code> is <code class="docutils literal notranslate"><span class="pre">f.trans</span> <span class="pre">g</span></code> also denoted by <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">&#8810;&#8811;&#8343;</span> <span class="pre">g</span></code>, and
the identity isomorphism of <code class="docutils literal notranslate"><span class="pre">V</span></code> is <code class="docutils literal notranslate"><span class="pre">LinearEquiv.refl</span> <span class="pre">K</span> <span class="pre">V</span></code>.
Elements of this type are automatically coerced to morphisms and functions when necessary.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8810;&#8811;&#8343;</span><span class="w"> </span><span class="n">f.symm</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">LinearEquiv.refl</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.self_trans_symm</span>
</pre></div>
</div>
<p>One can use <code class="docutils literal notranslate"><span class="pre">LinearEquiv.ofBijective</span></code> to build an isomorphism from a bijective morphism.
Doing so makes the inverse function noncomputable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Function.Bijective</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="bp">.</span><span class="n">ofBijective</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>Note that in the above example, Lean uses the announced type to understand that <code class="docutils literal notranslate"><span class="pre">.ofBijective</span></code>
refers to <code class="docutils literal notranslate"><span class="pre">LinearEquiv.ofBijective</span></code> (without needing to open any namespace).</p>
</section>
<section id="sums-and-products-of-vector-spaces">
<h3><span class="section-number">10.1.3. </span>Sums and products of vector spaces<a class="headerlink" href="#sums-and-products-of-vector-spaces" title="Link to this heading">&#61633;</a></h3>
<p>We can build new vector spaces out of old ones using direct sums and direct
products.
Let us start with two vectors spaces. In this case there is no difference between sum and product,
and we can simply use the product type.
In the following snippet of code we simply show how to get all the structure maps (inclusions
and projections) as linear maps, as well as the universal properties constructing linear maps
into products and out of sums (if you are not familiar with the category-theoretic distinction
between sums and products, you can simply ignore the universal property vocabulary and focus
on the types of the following examples).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">binary_product</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">W</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">]</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">U</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">U</span><span class="o">]</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">T</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">T</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">T</span><span class="o">]</span>

<span class="c1">-- First projection map</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.fst</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span>

<span class="c1">-- Second projection map</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.snd</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span>

<span class="c1">-- Universal property of the product</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w">  </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.prod</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span>

<span class="c1">-- The product map does the expected thing, first component</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearMap.fst</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">LinearMap.prod</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>

<span class="c1">-- The product map does the expected thing, second component</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearMap.snd</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">LinearMap.prod</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>

<span class="c1">-- We can also combine maps in parallel</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">T</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">T</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">&#966;.prodMap</span><span class="w"> </span><span class="n">&#968;</span>

<span class="c1">-- This is simply done by combining the projections with the universal property</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">T</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">  </span><span class="n">&#966;.prodMap</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="bp">.</span><span class="n">fst</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="bp">.</span><span class="n">prod</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="bp">.</span><span class="n">snd</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>

<span class="c1">-- First inclusion map</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.inl</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span>

<span class="c1">-- Second inclusion map</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.inr</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span>

<span class="c1">-- Universal property of the sum (aka coproduct)</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">&#966;.coprod</span><span class="w"> </span><span class="n">&#968;</span>

<span class="c1">-- The coproduct map does the expected thing, first component</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.coprod</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">LinearMap.inl</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">LinearMap.coprod_inl</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span>

<span class="c1">-- The coproduct map does the expected thing, second component</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.coprod</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">LinearMap.inr</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">LinearMap.coprod_inr</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span>

<span class="c1">-- The coproduct map is defined in the expected way</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">w</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">&#966;.coprod</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="o">,</span><span class="w"> </span><span class="n">w</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="n">w</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">end</span><span class="w"> </span><span class="n">binary_product</span>
</pre></div>
</div>
<p>Let us now turn to sums and products of arbitrary families of vector spaces.
Here we will simply see how to define a family of vector spaces and access the universal
properties of sums and products.
Note that the direct sum notation is scoped to the <code class="docutils literal notranslate"><span class="pre">DirectSum</span></code> namespace, and
that the universal property of direct sums requires decidable equality on the
indexing type (this is somehow an implementation accident).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">families</span>
<span class="kn">open</span><span class="w"> </span><span class="n">DirectSum</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span>
<span class="w">         </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">AddCommGroup</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)]</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)]</span>

<span class="c1">-- The universal property of the direct sum assembles maps from the summands to build</span>
<span class="c1">-- a map from the direct sum</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#10753;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">DirectSum.toModule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="n">&#966;</span>

<span class="c1">-- The universal property of the direct product assembles maps into the factors</span>
<span class="c1">-- to build a map into the direct product</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="o">(</span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">LinearMap.pi</span><span class="w"> </span><span class="n">&#966;</span>

<span class="c1">--&#8239;The projection maps from the product</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#928;</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">j</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.proj</span><span class="w"> </span><span class="n">i</span>

<span class="c1">-- The inclusion maps into the sum</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="bp">&#10753;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">DirectSum.lof</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span>

<span class="c1">-- The inclusion maps into the product</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.single</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span>

<span class="c1">-- In case `&#953;` is a finite type, there is an isomorphism between the sum and product.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#10753;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">linearEquivFunOnFintype</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">V</span>

<span class="kd">end</span><span class="w"> </span><span class="n">families</span>
</pre></div>
</div>
</section>
</section>
<section id="subspaces-and-quotients">
<span id="index-2"></span><h2><span class="section-number">10.2. </span>Subspaces and quotients<a class="headerlink" href="#subspaces-and-quotients" title="Link to this heading">&#61633;</a></h2>
<section id="subspaces">
<h3><span class="section-number">10.2.1. </span>Subspaces<a class="headerlink" href="#subspaces" title="Link to this heading">&#61633;</a></h3>
<p>Just as linear maps are bundled, a linear subspace of <code class="docutils literal notranslate"><span class="pre">V</span></code> is also a bundled structure consisting of
a set in <code class="docutils literal notranslate"><span class="pre">V</span></code>, called the carrier of the subspace, with the relevant closure properties.
Again the word module appears instead of vector space because of the more general context that
Mathlib actually uses for linear algebra.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Field</span><span class="w"> </span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hx</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">U.add_mem</span><span class="w"> </span><span class="n">hx</span><span class="w"> </span><span class="n">hy</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hx</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">U.smul_mem</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">hx</span>
</pre></div>
</div>
<p>In the example above, it is important to understand that <code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code> is the type of <code class="docutils literal notranslate"><span class="pre">K</span></code>-linear
subspaces of <code class="docutils literal notranslate"><span class="pre">V</span></code>, rather than a predicate <code class="docutils literal notranslate"><span class="pre">IsSubmodule</span> <span class="pre">U</span></code> where <code class="docutils literal notranslate"><span class="pre">U</span></code> is an element of <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">V</span></code>.
<code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code> is endowed with a coercion to <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">V</span></code> and a membership predicate on <code class="docutils literal notranslate"><span class="pre">V</span></code>.
See <a class="reference internal" href="C08_Hierarchies.html#section-hierarchies-subobjects"><span class="std std-numref">Section 8.3</span></a> for an explanation of how and why this is done.</p>
<p>Of course, two subspaces are the same if and only if they have the same elements. This fact
is registered for use with the <code class="docutils literal notranslate"><span class="pre">ext</span></code> tactic, which can be used to prove two subspaces are
equal in the same way it is used to prove that two sets are equal.</p>
<p>To state and prove, for example, that <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> is a <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>-linear subspace of <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>,
what we really want is to construct a term of type <code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">&#8477;</span> <span class="pre">&#8450;</span></code> whose projection to
<code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">&#8450;</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>, or, more precisely, the image of <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> in <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">&#8450;</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">carrier</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Set.range</span><span class="w"> </span><span class="o">((</span><span class="bp">&#8593;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8450;</span><span class="o">)</span>
<span class="w">  </span><span class="n">add_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rintro</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">rfl</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">rfl</span><span class="o">&#10217;</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">m</span>
<span class="w">    </span><span class="n">simp</span>
<span class="w">  </span><span class="n">zero_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="mi">0</span>
<span class="w">    </span><span class="n">simp</span>
<span class="w">  </span><span class="n">smul_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rintro</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">rfl</span><span class="o">&#10217;</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="n">c</span><span class="bp">*</span><span class="n">a</span>
<span class="w">    </span><span class="n">simp</span>
</pre></div>
</div>
<p>The prime at the end of proof fields in <code class="docutils literal notranslate"><span class="pre">Submodule</span></code> are analogous to the one in <code class="docutils literal notranslate"><span class="pre">LinearMap</span></code>.
Those fields are stated in terms of the <code class="docutils literal notranslate"><span class="pre">carrier</span></code> field because they are defined before the
<code class="docutils literal notranslate"><span class="pre">MemberShip</span></code> instance.&#8239;They are then superseded by <code class="docutils literal notranslate"><span class="pre">Submodule.add_mem</span></code>, <code class="docutils literal notranslate"><span class="pre">Submodule.zero_mem</span></code>
and <code class="docutils literal notranslate"><span class="pre">Submodule.smul_mem</span></code> that we saw above.</p>
<p>As an exercise in manipulating subspaces and linear maps, you will define the pre-image of
a subspace by a linear map (of course we will see below that Mathlib already knows about this).
Remember that <code class="docutils literal notranslate"><span class="pre">Set.mem_preimage</span></code> can be used to rewrite a statement involving
membership and preimage. This is the only lemma you will need in addition to the lemmas
discussed above about <code class="docutils literal notranslate"><span class="pre">LinearMap</span></code> and <code class="docutils literal notranslate"><span class="pre">Submodule</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">preimage</span><span class="w"> </span><span class="o">{</span><span class="n">W</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">carrier</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8315;&#185;&#39;</span><span class="w"> </span><span class="n">H</span>
<span class="w">  </span><span class="n">zero_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">add_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">smul_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Using type classes, Mathlib knows that a subspace of a vector space inherits a vector space structure.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>This example is subtle. The object <code class="docutils literal notranslate"><span class="pre">U</span></code> is not a type, but Lean automatically coerces it to
a type by interpreting it as a subtype of <code class="docutils literal notranslate"><span class="pre">V</span></code>.
So the above example can be restated more explicitly as:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">U</span><span class="o">}</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
</section>
<section id="complete-lattice-structure-and-internal-direct-sums">
<h3><span class="section-number">10.2.2. </span>Complete lattice structure and internal direct sums<a class="headerlink" href="#complete-lattice-structure-and-internal-direct-sums" title="Link to this heading">&#61633;</a></h3>
<p>An important benefit of having a type <code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code> instead of a predicate
<code class="docutils literal notranslate"><span class="pre">IsSubmodule</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">V</span> <span class="pre">&#8594;</span> <span class="pre">Prop</span></code> is that one can easily endow <code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code> with additional structure.
Importantly, it has the structure of a complete lattice structure with respect to
inclusion. For instance, instead of having a lemma stating that an intersection of
two subspaces of <code class="docutils literal notranslate"><span class="pre">V</span></code> is again a subspace, we
use the lattice operation <code class="docutils literal notranslate"><span class="pre">&#8851;</span></code> to construct the intersection. We can then apply arbitrary
lemmas about lattices to the construction.</p>
<p>Let us check that the set underlying the infimum of two subspaces is indeed, by definition,
their intersection.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">((</span><span class="n">H</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It may look strange to have a different notation for what amounts to the intersection of the
underlying sets, but the correspondence does not carry over to the supremum operation and set
union, since a union of subspaces is not, in general, a subspace.
Instead one needs to use the subspace generated by the union, which is done
using <code class="docutils literal notranslate"><span class="pre">Submodule.span</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">((</span><span class="n">H</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Submodule.span</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">((</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="o">(</span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">V</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">Submodule.span_union</span><span class="o">]</span>
</pre></div>
</div>
<p>Another subtlety is that <code class="docutils literal notranslate"><span class="pre">V</span></code> itself does not have type <code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code>,
so we need a way to talk about <code class="docutils literal notranslate"><span class="pre">V</span></code> seen as a subspace of <code class="docutils literal notranslate"><span class="pre">V</span></code>.
This is also provided by the lattice structure: the full subspace is the top element of
this lattice.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8868;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">trivial</span>
</pre></div>
</div>
<p>Similarly the bottom element of this lattice is the subspace whose only element is the
zero element.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Submodule.mem_bot</span><span class="w"> </span><span class="n">K</span>
</pre></div>
</div>
<p>In particular we can discuss the case of subspaces that are in (internal) direct sum.
In the case of two subspaces, we use the general purpose predicate <code class="docutils literal notranslate"><span class="pre">IsCompl</span></code>
which makes sense for any bounded partially ordered type.
In the case of general families of subspaces we use <code class="docutils literal notranslate"><span class="pre">DirectSum.IsInternal</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c1">-- If two subspaces are in direct sum then they span the whole space.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsCompl</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">  </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8868;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">h.sup_eq_top</span>

<span class="c1">-- If two subspaces are in direct sum then they intersect only at zero.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsCompl</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">  </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">h.inf_eq_bot</span>

<span class="kn">section</span>
<span class="kn">open</span><span class="w"> </span><span class="n">DirectSum</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span>

<span class="c1">-- If subspaces are in direct sum then they span the whole space.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DirectSum.IsInternal</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">  </span><span class="bp">&#10758;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8868;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">h.submodule_iSup_eq_top</span>

<span class="c1">-- If subspaces are in direct sum then they pairwise intersect only at zero.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DirectSum.IsInternal</span><span class="w"> </span><span class="n">U</span><span class="o">)</span>
<span class="w">    </span><span class="o">{</span><span class="n">i</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hij</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">j</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">h.submodule_iSupIndep.pairwiseDisjoint</span><span class="w"> </span><span class="n">hij</span><span class="o">)</span><span class="bp">.</span><span class="n">eq_bot</span>

<span class="c1">-- Those conditions characterize direct sums.</span>
<span class="k">#check</span><span class="w"> </span><span class="n">DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top</span>

<span class="c1">-- The relation with external direct sums: if a family of subspaces is</span>
<span class="c1">-- in internal direct sum then the map from their external direct sum into `V`</span>
<span class="c1">-- is a linear isomorphism.</span>
<span class="kd">noncomputable</span><span class="w"> </span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DirectSum.IsInternal</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#10753;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">LinearEquiv.ofBijective</span><span class="w"> </span><span class="o">(</span><span class="n">coeLinearMap</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="n">h</span>
<span class="kd">end</span>
</pre></div>
</div>
</section>
<section id="subspace-spanned-by-a-set">
<h3><span class="section-number">10.2.3. </span>Subspace spanned by a set<a class="headerlink" href="#subspace-spanned-by-a-set" title="Link to this heading">&#61633;</a></h3>
<p>In addition to building subspaces out of existing subspaces, we can build them out
of any set <code class="docutils literal notranslate"><span class="pre">s</span></code> using <code class="docutils literal notranslate"><span class="pre">Submodule.span</span> <span class="pre">K</span> <span class="pre">s</span></code> which builds the smallest subspace
containing <code class="docutils literal notranslate"><span class="pre">s</span></code>.
On paper it is common to use that this space is made of all linear combinations of elements of
<code class="docutils literal notranslate"><span class="pre">s</span></code>.
But it is often more efficient to use its universal property expressed by <code class="docutils literal notranslate"><span class="pre">Submodule.span_le</span></code>,
and the whole theory of Galois connections.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">V</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule.span</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Submodule.span_le</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaloisInsertion</span><span class="w"> </span><span class="o">(</span><span class="n">Submodule.span</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">((</span><span class="bp">&#8593;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Submodule.gi</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span>
</pre></div>
</div>
<p>When those are not enough, one can use the relevant induction principle
<code class="docutils literal notranslate"><span class="pre">Submodule.span_induction</span></code> which ensures a property holds for every element of the
span of <code class="docutils literal notranslate"><span class="pre">s</span></code> as long as it holds on <code class="docutils literal notranslate"><span class="pre">zero</span></code> and elements of <code class="docutils literal notranslate"><span class="pre">s</span></code> and is stable under
sum and scalar multiplication.</p>
<p>As an exercise, let us reprove one implication of <code class="docutils literal notranslate"><span class="pre">Submodule.mem_sup</span></code>.
Remember that you can use the <cite>module</cite> tactic to close goals that follow from
the axioms relating the various algebraic operations on <code class="docutils literal notranslate"><span class="pre">V</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">S</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">T</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">S</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">T</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">t</span><span class="w">  </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">S.span_eq</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">T.span_eq</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">Submodule.span_union</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">induction</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Submodule.span_induction</span><span class="w"> </span><span class="k">with</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">mem</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="gr">sorry</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="gr">sorry</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">hx</span><span class="w"> </span><span class="n">hy</span><span class="w"> </span><span class="n">hx&#39;</span><span class="w"> </span><span class="n">hy&#39;</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="gr">sorry</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">smul</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">hx</span><span class="w"> </span><span class="n">hx&#39;</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="pushing-and-pulling-subspaces">
<h3><span class="section-number">10.2.4. </span>Pushing and pulling subspaces<a class="headerlink" href="#pushing-and-pulling-subspaces" title="Link to this heading">&#61633;</a></h3>
<p>As promised earlier, we now describe how to push and pull subspaces by linear maps.
As usual in Mathlib, the first operation is called <code class="docutils literal notranslate"><span class="pre">map</span></code> and the second one is called
<code class="docutils literal notranslate"><span class="pre">comap</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">W</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="k">in</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Submodule.map</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="k">in</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Submodule.comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
</pre></div>
</div>
<p>Note those live in the <code class="docutils literal notranslate"><span class="pre">Submodule</span></code> namespace so one can use dot notation and write
<code class="docutils literal notranslate"><span class="pre">E.map</span> <span class="pre">&#966;</span></code> instead of <code class="docutils literal notranslate"><span class="pre">Submodule.map</span> <span class="pre">&#966;</span> <span class="pre">E</span></code>, but this is pretty awkward to read (although some
Mathlib contributors use this spelling).</p>
<p>In particular the range and kernel of a linear map are subspaces. Those special cases are important
enough to get declarations.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearMap.range</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">.</span><span class="n">map</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8868;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.range_eq_map</span><span class="w"> </span><span class="n">&#966;</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearMap.ker</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">.</span><span class="n">comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Submodule.comap_bot</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="c1">-- or `rfl`</span>
</pre></div>
</div>
<p>Note that we cannot write <code class="docutils literal notranslate"><span class="pre">&#966;.ker</span></code> instead of <code class="docutils literal notranslate"><span class="pre">LinearMap.ker</span> <span class="pre">&#966;</span></code> because <code class="docutils literal notranslate"><span class="pre">LinearMap.ker</span></code> also
applies to classes of maps preserving more structure, hence it does not expect an argument
whose type starts with <code class="docutils literal notranslate"><span class="pre">LinearMap</span></code>, hence dot notation doesn&#8217;t work here.
However we were able to use the other flavor of dot notation in the right-hand side. Because
Lean expects a term with type <code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code> after elaborating the left-hand side, it interprets
<code class="docutils literal notranslate"><span class="pre">.comap</span></code> as <code class="docutils literal notranslate"><span class="pre">Submodule.comap</span></code>.</p>
<p>The following lemmas give the key relations between those submodule and the properties of <code class="docutils literal notranslate"><span class="pre">&#966;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Function</span><span class="w"> </span><span class="n">LinearMap</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Injective</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">ker_eq_bot.symm</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Surjective</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8868;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">range_eq_top.symm</span>
</pre></div>
</div>
<p>As an exercise, let us prove the Galois connection property for <code class="docutils literal notranslate"><span class="pre">map</span></code> and <code class="docutils literal notranslate"><span class="pre">comap</span></code>.
One can use the following lemmas but this is not required since they are true by definition.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Submodule.mem_map_of_mem</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.mem_map</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.mem_comap</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Submodule.map</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">Submodule.comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="quotient-spaces">
<h3><span class="section-number">10.2.5. </span>Quotient spaces<a class="headerlink" href="#quotient-spaces" title="Link to this heading">&#61633;</a></h3>
<p>Quotient vector spaces use the general quotient notation (typed with <code class="docutils literal notranslate"><span class="pre">\quot</span></code>, not the ordinary
<code class="docutils literal notranslate"><span class="pre">/</span></code>).
The projection onto a quotient space is <code class="docutils literal notranslate"><span class="pre">Submodule.mkQ</span></code> and the universal property is
<code class="docutils literal notranslate"><span class="pre">Submodule.liftQ</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">E.mkQ</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="n">E.mkQ</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">E.ker_mkQ</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">E.mkQ</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8868;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">E.range_mkQ</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">E.liftQ</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">h&#966;</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">.</span><span class="n">comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">E.mapQ</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">h&#966;</span>

<span class="kd">noncomputable</span><span class="w"> </span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">LinearMap.ker</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">&#966;.quotKerEquivRange</span>
</pre></div>
</div>
<p>As an exercise, let us prove the correspondence theorem for subspaces of quotient spaces.
Mathlib knows a slightly more precise version as <code class="docutils literal notranslate"><span class="pre">Submodule.comapMkQRelIso</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Submodule</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.map_comap_eq</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.comap_map_eq</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="o">{</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">}</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">toFun</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">invFun</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">left_inv</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">right_inv</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
</pre></div>
</div>
</section>
</section>
<section id="endomorphisms">
<h2><span class="section-number">10.3. </span>Endomorphisms<a class="headerlink" href="#endomorphisms" title="Link to this heading">&#61633;</a></h2>
<p>An important special case of linear maps are endomorphisms: linear maps from a vector space to itself.
They are interesting because they form a <code class="docutils literal notranslate"><span class="pre">K</span></code>-algebra. In particular we can evaluate polynomials
with coefficients in <code class="docutils literal notranslate"><span class="pre">K</span></code> on them, and they can have eigenvalues and eigenvectors.</p>
<p>Mathlib uses the abbreviation <code class="docutils literal notranslate"><span class="pre">Module.End</span> <span class="pre">K</span> <span class="pre">V</span> <span class="pre">:=</span> <span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">V</span></code> which is convenient when
using a lot of these (especially after opening the <code class="docutils literal notranslate"><span class="pre">Module</span></code> namespace).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Field</span><span class="w"> </span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">W</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">]</span>


<span class="kn">open</span><span class="w"> </span><span class="n">Polynomial</span><span class="w"> </span><span class="n">Module</span><span class="w"> </span><span class="n">LinearMap</span><span class="w"> </span><span class="n">End</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">End.mul_eq_comp</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="c1">-- `rfl` would also work</span>

<span class="c1">-- evaluating `P` on `&#966;`</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">P</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">P</span>

<span class="c1">-- evaluating `X` on `&#966;` gives back `&#966;`</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">aeval_X</span><span class="w"> </span><span class="n">&#966;</span>
</pre></div>
</div>
<p>As an exercise manipulating endomorphisms, subspaces and polynomials, let us prove the
(binary) kernels lemma: for any endomorphism <span class="math notranslate nohighlight">\(&#966;\)</span> and any two relatively
prime polynomials <span class="math notranslate nohighlight">\(P\)</span> and <span class="math notranslate nohighlight">\(Q\)</span>, we have <span class="math notranslate nohighlight">\(\ker P(&#966;) &#8853; \ker Q(&#966;) = \ker \big(PQ(&#966;)\big)\)</span>.</p>
<p>Note that <code class="docutils literal notranslate"><span class="pre">IsCoprime</span> <span class="pre">x</span> <span class="pre">y</span></code> is defined as <code class="docutils literal notranslate"><span class="pre">&#8707;</span> <span class="pre">a</span> <span class="pre">b,</span> <span class="pre">a</span> <span class="pre">*</span> <span class="pre">x</span> <span class="pre">+</span> <span class="pre">b</span> <span class="pre">*</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">1</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Submodule.eq_bot_iff</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.mem_inf</span>
<span class="k">#check</span><span class="w"> </span><span class="n">LinearMap.mem_ker</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">P</span><span class="w"> </span><span class="n">Q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="n">Q</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="o">(</span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">P</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="o">(</span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">Q</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.add_mem_sup</span>
<span class="k">#check</span><span class="w"> </span><span class="n">map_mul</span>
<span class="k">#check</span><span class="w"> </span><span class="n">End.mul_apply</span>
<span class="k">#check</span><span class="w"> </span><span class="n">LinearMap.ker_le_ker_comp</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">P</span><span class="w"> </span><span class="n">Q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="n">Q</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">ker</span><span class="w"> </span><span class="o">(</span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">P</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="o">(</span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">Q</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="o">(</span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">P</span><span class="bp">*</span><span class="n">Q</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We now move to the discussions of eigenspaces and eigenvalues. The eigenspace
associated to an endomorphism <span class="math notranslate nohighlight">\(&#966;\)</span> and a scalar <span class="math notranslate nohighlight">\(a\)</span> is the kernel of <span class="math notranslate nohighlight">\(&#966; - aId\)</span>.
Eigenspaces are defined for all values of <code class="docutils literal notranslate"><span class="pre">a</span></code>, although
they are interesting only when they are non-zero.
However an eigenvector is, by definition, a non-zero element of an eigenspace. The corresponding
predicate is <code class="docutils literal notranslate"><span class="pre">End.HasEigenvector</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.eigenspace</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">LinearMap.ker</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">End.eigenspace_def</span>
</pre></div>
</div>
<p>Then there is a predicate <code class="docutils literal notranslate"><span class="pre">End.HasEigenvalue</span></code> and the corresponding subtype <code class="docutils literal notranslate"><span class="pre">End.Eigenvalues</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.HasEigenvalue</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">&#966;.eigenspace</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Iff.rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.HasEigenvalue</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">v</span><span class="o">,</span><span class="w"> </span><span class="n">&#966;.HasEigenvector</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">v</span><span class="w">  </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">End.HasEigenvalue.exists_hasEigenvector</span><span class="o">,</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">_</span><span class="o">,</span><span class="w"> </span><span class="n">hv</span><span class="o">&#10217;</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">&#966;.hasEigenvalue_of_hasEigenvector</span><span class="w"> </span><span class="n">hv</span><span class="o">&#10217;</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.Eigenvalues</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="n">&#966;.HasEigenvalue</span><span class="w"> </span><span class="n">a</span><span class="o">}</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="c1">-- Eigenvalue are roots of the minimal polynomial</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.HasEigenvalue</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="o">(</span><span class="n">minpoly</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="bp">.</span><span class="n">IsRoot</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">&#966;.isRoot_of_hasEigenvalue</span>

<span class="c1">-- In finite dimension, the converse is also true (we will discuss dimension below)</span>
<span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">&#966;.HasEigenvalue</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="o">(</span><span class="n">minpoly</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="bp">.</span><span class="n">IsRoot</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">&#966;.hasEigenvalue_iff_isRoot</span>

<span class="c1">--&#8239;Cayley-Hamilton</span>
<span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#966;.charpoly</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">&#966;.aeval_self_charpoly</span>
</pre></div>
</div>
</section>
<section id="matrices-bases-and-dimension">
<span id="matrices-bases-dimension"></span><h2><span class="section-number">10.4. </span>Matrices, bases and dimension<a class="headerlink" href="#matrices-bases-and-dimension" title="Link to this heading">&#61633;</a></h2>
<section id="matrices">
<span id="id2"></span><h3><span class="section-number">10.4.1. </span>Matrices<a class="headerlink" href="#matrices" title="Link to this heading">&#61633;</a></h3>
<p id="index-3">Before introducing bases for abstract vector spaces, we go back to the much more elementary setup
of linear algebra in <span class="math notranslate nohighlight">\(K^n\)</span> for some field <span class="math notranslate nohighlight">\(K\)</span>.
Here the main objects are vectors and matrices.
For concrete vectors, one can use the <code class="docutils literal notranslate"><span class="pre">![&#8230;]</span></code> notation, where components are separated by commas.
For concrete matrices we can use the <code class="docutils literal notranslate"><span class="pre">!![&#8230;]</span></code> notation, lines are separated by semi-colons
and components of lines are separated by colons.
When entries have a computable type such as <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> or <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code>, we can use
the <code class="docutils literal notranslate"><span class="pre">eval</span></code> command to play with basic operations.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">matrices</span>

<span class="c1">-- Adding vectors</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">]</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="w">  </span><span class="c1">-- ![4, 6]</span>

<span class="c1">-- Adding matrices</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="bp">;</span><span class="w"> </span><span class="mi">5</span><span class="o">,</span><span class="w"> </span><span class="mi">6</span><span class="o">]</span><span class="w">  </span><span class="c1">-- !![4, 6; 8, 10]</span>

<span class="c1">-- Multiplying matrices</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="bp">;</span><span class="w"> </span><span class="mi">5</span><span class="o">,</span><span class="w"> </span><span class="mi">6</span><span class="o">]</span><span class="w">  </span><span class="c1">-- !![13, 16; 29, 36]</span>
</pre></div>
</div>
<p>It is important to understand that this use of <code class="docutils literal notranslate"><span class="pre">#eval</span></code> is interesting only for
exploration, it is not meant to replace a computer algebra system such as Sage.
The data representation used here for matrices is <em>not</em> computationally
efficient in any way. It uses functions instead of arrays and is optimized for
proving, not computing.
The virtual machine used by <code class="docutils literal notranslate"><span class="pre">#eval</span></code> is also not optimized for this use.</p>
<p>Beware the matrix notation list rows but the vector notation
is neither a row vector nor a column vector. Multiplication of a matrix with a vector
from the left (resp. right) interprets the vector as a row (resp. column) vector.
This corresponds to operations
<code class="docutils literal notranslate"><span class="pre">Matrix.vecMul</span></code>, with notation <code class="docutils literal notranslate"><span class="pre">&#7525;*</span></code> and <code class="docutils literal notranslate"><span class="pre">Matrix.mulVec</span></code>, with notation ` <cite>*&#7525;`</cite>.
Those notations are scoped in the <code class="docutils literal notranslate"><span class="pre">Matrix</span></code> namespace that we therefore need to open.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Matrix</span>

<span class="c1">-- matrices acting on vectors on the left</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="w"> </span><span class="bp">*&#7525;</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span><span class="w"> </span><span class="c1">-- ![3, 7]</span>

<span class="c1">-- matrices acting on vectors on the left, resulting in a size one matrix</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">]</span><span class="w"> </span><span class="bp">*&#7525;</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span><span class="w">  </span><span class="c1">-- ![3]</span>

<span class="c1">-- matrices acting on vectors on the right</span>
<span class="k">#eval</span><span class="w">  </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span><span class="w"> </span><span class="bp">&#7525;*</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="bp">;</span><span class="w"> </span><span class="mi">5</span><span class="o">,</span><span class="w"> </span><span class="mi">6</span><span class="o">]</span><span class="w"> </span><span class="c1">-- ![9, 12]</span>
</pre></div>
</div>
<p>In order to generate matrices with identical rows or columns specified by a vector, we
use <code class="docutils literal notranslate"><span class="pre">Matrix.replicateRow</span></code> and <code class="docutils literal notranslate"><span class="pre">Matrix.replicateCol</span></code>, with arguments the type indexing the
rows or columns and the vector.
For instance one can get single row or single column matrixes (more precisely matrices whose rows
or columns are indexed by <code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">1</span></code>).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#eval</span><span class="w"> </span><span class="n">replicateRow</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">]</span><span class="w"> </span><span class="c1">-- !![1, 2]</span>

<span class="k">#eval</span><span class="w"> </span><span class="n">replicateCol</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">]</span><span class="w"> </span><span class="c1">-- !![1; 2]</span>
</pre></div>
</div>
<p>Other familiar operations include the vector dot product, matrix transpose, and,
for square matrices, determinant and trace.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c1">-- vector dot product</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">]</span><span class="w"> </span><span class="bp">&#11037;&#7525;</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="w"> </span><span class="c1">-- `11`</span>

<span class="c1">-- matrix transpose</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="bp">&#7488;</span><span class="w"> </span><span class="c1">-- `!![1, 3; 2, 4]`</span>

<span class="c1">-- determinant</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="c1">-- `-2`</span>

<span class="c1">-- trace</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="bp">.</span><span class="n">trace</span><span class="w"> </span><span class="c1">-- `5`</span>
</pre></div>
</div>
<p>When entries do not have a computable type, for instance if they are real numbers, we cannot
hope that <code class="docutils literal notranslate"><span class="pre">#eval</span></code> can help. Also this kind of evaluation cannot be used in proofs without
considerably expanding the trusted code base (i.e. the part of Lean that you need to trust when
checking proofs).</p>
<p>So it is good to also use the <code class="docutils literal notranslate"><span class="pre">simp</span></code> and <code class="docutils literal notranslate"><span class="pre">norm_num</span></code> tactics in proofs, or
their command counter-part for quick exploration.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">#</span><span class="n">simp</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="c1">-- `4 - 2*3`</span>

<span class="bp">#</span><span class="n">norm_num</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="c1">-- `-2`</span>

<span class="bp">#</span><span class="n">norm_num</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="bp">.</span><span class="n">trace</span><span class="w"> </span><span class="c1">-- `5`</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="k">in</span>
<span class="bp">#</span><span class="n">simp</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">b</span><span class="bp">;</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">d</span><span class="o">]</span><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="c1">-- `a * d &#8211; b * c`</span>
</pre></div>
</div>
<p>The next important operation on square matrices is inversion.
In the same way as division of numbers is always defined and returns the artificial value
zero for division by zero, the inversion operation is defined on all matrices and returns
the zero matrix for non-invertible matrices.</p>
<p>More precisely, there is general function <code class="docutils literal notranslate"><span class="pre">Ring.inverse</span></code> that does this in any ring,
and, for any matrix <code class="docutils literal notranslate"><span class="pre">A</span></code>, <code class="docutils literal notranslate"><span class="pre">A&#8315;&#185;</span></code> is defined as <code class="docutils literal notranslate"><span class="pre">Ring.inverse</span> <span class="pre">A.det</span> <span class="pre">&#8226;</span> <span class="pre">A.adjugate</span></code>.
According to Cramer&#8217;s rule, this is indeed the inverse of <code class="docutils literal notranslate"><span class="pre">A</span></code> when the determinant of <code class="docutils literal notranslate"><span class="pre">A</span></code> is
not zero.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">#</span><span class="n">norm_num</span><span class="w"> </span><span class="o">[</span><span class="n">Matrix.inv_def</span><span class="o">]</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="c1">-- !![-2, 1; 3 / 2, -(1 / 2)]</span>
</pre></div>
</div>
<p>Of course this definition is really useful only for invertible matrices.
There is a general type class <code class="docutils literal notranslate"><span class="pre">Invertible</span></code> that helps recording this.
For instance, the <code class="docutils literal notranslate"><span class="pre">simp</span></code> call in the next example will use the <code class="docutils literal notranslate"><span class="pre">inv_mul_of_invertible</span></code>
lemma which has an <code class="docutils literal notranslate"><span class="pre">Invertible</span></code> type-class assumption, so it will trigger
only if this can be found by the type-class synthesis system.
Here we make this fact available using a <code class="docutils literal notranslate"><span class="pre">have</span></code> statement.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Invertible</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">Matrix.invertibleOfIsUnitDet</span>
<span class="w">    </span><span class="n">norm_num</span>
<span class="w">  </span><span class="n">simp</span>
</pre></div>
</div>
<p>In this fully concrete case, we could also use the <code class="docutils literal notranslate"><span class="pre">norm_num</span></code> machinery,
and <code class="docutils literal notranslate"><span class="pre">apply?</span></code> to find the final line:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">norm_num</span><span class="w"> </span><span class="o">[</span><span class="n">Matrix.inv_def</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">one_fin_two.symm</span>
</pre></div>
</div>
<p>All the concrete matrices above have their rows and columns indexed by <code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">n</span></code> for
some <code class="docutils literal notranslate"><span class="pre">n</span></code> (not necessarily the same for rows and columns).
But sometimes it is more convenient to index matrices using arbitrary finite types.
For instance the adjacency matrix of a finite graph has rows and columns naturally indexed by
the vertices of the graph.</p>
<p>In fact when simply wants to define matrices without defining any operation on them,
finiteness of the indexing types are not even needed, and coefficients can have any type,
without any algebraic structure.
So Mathlib simply defines <code class="docutils literal notranslate"><span class="pre">Matrix</span> <span class="pre">m</span> <span class="pre">n</span> <span class="pre">&#945;</span></code> to be <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">&#8594;</span> <span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">&#945;</span></code> for any types <code class="docutils literal notranslate"><span class="pre">m</span></code>, <code class="docutils literal notranslate"><span class="pre">n</span></code> and <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>,
and the matrices we have been using so far had types such as <code class="docutils literal notranslate"><span class="pre">Matrix</span> <span class="pre">(Fin</span> <span class="pre">2)</span> <span class="pre">(Fin</span> <span class="pre">2)</span> <span class="pre">&#8477;</span></code>.
Of course algebraic operations require more assumptions on <code class="docutils literal notranslate"><span class="pre">m</span></code>, <code class="docutils literal notranslate"><span class="pre">n</span></code> and <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.</p>
<p>Note the main reason why we do not use <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">&#8594;</span> <span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">&#945;</span></code> directly is to allow the type class
system to understand what we want. For instance, for a ring <code class="docutils literal notranslate"><span class="pre">R</span></code>, the type <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">R</span></code> is
endowed with the point-wise multiplication operation, and similarly <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">&#8594;</span> <span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">R</span></code>
has this operation which is <em>not</em> the multiplication we want on matrices.</p>
<p>In the first example below, we force Lean to see through the definition of <code class="docutils literal notranslate"><span class="pre">Matrix</span></code>
and accept the statement as meaningful, and then prove it by checking all entries.</p>
<p>But then the next two examples reveal that Lean uses the point-wise multiplication
on <code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">2</span> <span class="pre">&#8594;</span> <span class="pre">Fin</span> <span class="pre">2</span> <span class="pre">&#8594;</span> <span class="pre">&#8484;</span></code> but the matrix multiplication on <code class="docutils literal notranslate"><span class="pre">Matrix</span> <span class="pre">(Fin</span> <span class="pre">2)</span> <span class="pre">(Fin</span> <span class="pre">2)</span> <span class="pre">&#8484;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="bp">;</span><span class="w"> </span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span>
<span class="w">  </span><span class="n">fin_cases</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">fin_cases</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="bp">;</span><span class="w"> </span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span>
<span class="w">  </span><span class="n">fin_cases</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">fin_cases</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="bp">;</span><span class="w"> </span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="bp">;</span><span class="w"> </span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">]</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">norm_num</span>
</pre></div>
</div>
<p>In order to define matrices as functions without losing the benefits of <code class="docutils literal notranslate"><span class="pre">Matrix</span></code>
for type class synthesis, we can use the equivalence <code class="docutils literal notranslate"><span class="pre">Matrix.of</span></code> between functions
and matrices.&#8239;This equivalence is secretly defined using <code class="docutils literal notranslate"><span class="pre">Equiv.refl</span></code>.</p>
<p>For instance we can define Vandermonde matrices corresponding to a vector <code class="docutils literal notranslate"><span class="pre">v</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Matrix.vandermonde</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Matrix.of</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="o">(</span><span class="n">j</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
<span class="kd">end</span>
<span class="kd">end</span><span class="w"> </span><span class="n">matrices</span>
</pre></div>
</div>
</section>
<section id="bases">
<h3><span class="section-number">10.4.2. </span>Bases<a class="headerlink" href="#bases" title="Link to this heading">&#61633;</a></h3>
<p>We now want to discuss bases of vector spaces. Informally there are many ways to define this notion.
One can use a universal property.
One can say a basis is a family of vectors that is linearly independent and spanning.
Or one can combine those properties and directly say that a basis is a family of vectors
such that every vectors can be written uniquely as a linear combination of bases vectors.
Yet another way to say it is that a basis provides a linear isomorphism with a power of
the base field <code class="docutils literal notranslate"><span class="pre">K</span></code>, seen as a vector space over <code class="docutils literal notranslate"><span class="pre">K</span></code>.</p>
<p>This isomorphism version is actually the one that Mathlib uses as a definition under the hood, and
other characterizations are proven from it.
One must be slightly careful with the &#8220;power of <code class="docutils literal notranslate"><span class="pre">K</span></code>&#8221; idea in the case of infinite bases.
Indeed only finite linear combinations make sense in this algebraic context. So what we need
as a reference vector space is not a direct product of copies of <code class="docutils literal notranslate"><span class="pre">K</span></code> but a direct sum.
We could use <code class="docutils literal notranslate"><span class="pre">&#10753;</span> <span class="pre">i</span> <span class="pre">:</span> <span class="pre">&#953;,</span> <span class="pre">K</span></code> for some type <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> indexing the basis
But we rather use the more specialized spelling <code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">&#8594;&#8320;</span> <span class="pre">K</span></code> which means
&#8220;functions from <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> to <code class="docutils literal notranslate"><span class="pre">K</span></code> with finite support&#8221;, i.e. functions which vanish outside a finite set
in <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> (this finite set is not fixed, it depends on the function).
Evaluating such a function coming from a basis <code class="docutils literal notranslate"><span class="pre">B</span></code> at a vector <code class="docutils literal notranslate"><span class="pre">v</span></code> and
<code class="docutils literal notranslate"><span class="pre">i</span> <span class="pre">:</span> <span class="pre">&#953;</span></code> returns the component (or coordinate) of <code class="docutils literal notranslate"><span class="pre">v</span></code> on the <code class="docutils literal notranslate"><span class="pre">i</span></code>-th basis vector.</p>
<p>The type of bases indexed by a type <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> of <code class="docutils literal notranslate"><span class="pre">V</span></code> as a <code class="docutils literal notranslate"><span class="pre">K</span></code> vector space is <code class="docutils literal notranslate"><span class="pre">Basis</span> <span class="pre">&#953;</span> <span class="pre">K</span> <span class="pre">V</span></code>.
The isomorphism is called <code class="docutils literal notranslate"><span class="pre">Basis.repr</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Field</span><span class="w"> </span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span>

<span class="kn">section</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">B</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span>

<span class="c1">-- The basis vector with index ``i``</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>

<span class="c1">-- the linear isomorphism with the model space given by ``B``</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B.repr</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;&#8320;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>

<span class="c1">-- the component function of ``v``</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B.repr</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;&#8320;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>

<span class="c1">-- the component of ``v`` with index ``i``</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B.repr</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>
</pre></div>
</div>
<p>Instead of starting with such an isomorphism, one can start with a family <code class="docutils literal notranslate"><span class="pre">b</span></code> of vectors that is
linearly independent and spanning, this is <code class="docutils literal notranslate"><span class="pre">Basis.mk</span></code>.</p>
<p>The assumption that the family is spanning is spelled out as <code class="docutils literal notranslate"><span class="pre">&#8868;</span> <span class="pre">&#8804;</span> <span class="pre">Submodule.span</span> <span class="pre">K</span> <span class="pre">(Set.range</span> <span class="pre">b)</span></code>.
Here <code class="docutils literal notranslate"><span class="pre">&#8868;</span></code> is the top submodule of <code class="docutils literal notranslate"><span class="pre">V</span></code>, i.e. <code class="docutils literal notranslate"><span class="pre">V</span></code> seen as submodule of itself.
This spelling looks a bit tortuous, but we will see below that it is almost equivalent by definition
to the more readable <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">v,</span> <span class="pre">v</span> <span class="pre">&#8712;</span> <span class="pre">Submodule.span</span> <span class="pre">K</span> <span class="pre">(Set.range</span> <span class="pre">b)</span></code> (the underscores in the snippet
below refers to the useless information <code class="docutils literal notranslate"><span class="pre">v</span> <span class="pre">&#8712;</span> <span class="pre">&#8868;</span></code>).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">b_indep</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearIndependent</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">b_spans</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">v</span><span class="o">,</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">Submodule.span</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">Set.range</span><span class="w"> </span><span class="n">b</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Basis.mk</span><span class="w"> </span><span class="n">b_indep</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">b_spans</span><span class="w"> </span><span class="n">v</span><span class="o">)</span>

<span class="c1">-- The family of vectors underlying the above basis is indeed ``b``.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">b_indep</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearIndependent</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">b_spans</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">v</span><span class="o">,</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">Submodule.span</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">Set.range</span><span class="w"> </span><span class="n">b</span><span class="o">))</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Basis.mk</span><span class="w"> </span><span class="n">b_indep</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">b_spans</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Basis.mk_apply</span><span class="w"> </span><span class="n">b_indep</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">b_spans</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="n">i</span>
</pre></div>
</div>
<p>In particular the model vector space <code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">&#8594;&#8320;</span> <span class="pre">K</span></code> has a so-called canonical basis whose <code class="docutils literal notranslate"><span class="pre">repr</span></code>
function evaluated on any vector is the identity isomorphism. It is called
<code class="docutils literal notranslate"><span class="pre">Finsupp.basisSingleOne</span></code> where <code class="docutils literal notranslate"><span class="pre">Finsupp</span></code> means function with finite support and
<code class="docutils literal notranslate"><span class="pre">basisSingleOne</span></code> refers to the fact that basis vectors are functions which
vanish expect for a single input value. More precisely the basis vector indexed by <code class="docutils literal notranslate"><span class="pre">i</span> <span class="pre">:</span> <span class="pre">&#953;</span></code>
is <code class="docutils literal notranslate"><span class="pre">Finsupp.single</span> <span class="pre">i</span> <span class="pre">1</span></code> which is the finitely supported function taking value <code class="docutils literal notranslate"><span class="pre">1</span></code> at <code class="docutils literal notranslate"><span class="pre">i</span></code>
and <code class="docutils literal notranslate"><span class="pre">0</span></code> everywhere else.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span>
</pre></div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finsupp.basisSingleOne.repr</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">LinearEquiv.refl</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;&#8320;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finsupp.basisSingleOne</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Finsupp.single</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>The story of finitely supported functions is unneeded when the indexing type is finite.
In this case we can use the simpler <code class="docutils literal notranslate"><span class="pre">Pi.basisFun</span></code> which gives a basis of the whole
<code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">&#8594;</span> <span class="pre">K</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">Finite</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="k">Pi</span><span class="bp">.</span><span class="n">basisFun</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="bp">.</span><span class="n">repr</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span>
</pre></div>
</div>
<p>Going back to the general case of bases of abstract vector spaces, we can express
any vector as a linear combination of basis vectors.
Let us first see the easy case of finite bases.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">,</span><span class="w"> </span><span class="n">B.repr</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="o">(</span><span class="n">B</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">B.sum_repr</span><span class="w"> </span><span class="n">v</span>
</pre></div>
</div>
<p>When <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> is not finite, the above statement makes no sense a priori: we cannot take a sum over <code class="docutils literal notranslate"><span class="pre">&#953;</span></code>.
However the support of the function being summed is finite (it is the support of <code class="docutils literal notranslate"><span class="pre">B.repr</span> <span class="pre">v</span></code>).
But we need to apply a construction that takes this into account.
Here Mathlib uses a special purpose function that requires some time to get used to:
<code class="docutils literal notranslate"><span class="pre">Finsupp.linearCombination</span></code> (which is built on top of the more general <code class="docutils literal notranslate"><span class="pre">Finsupp.sum</span></code>).
Given a finitely supported function <code class="docutils literal notranslate"><span class="pre">c</span></code> from a type <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> to the base field <code class="docutils literal notranslate"><span class="pre">K</span></code> and any
function <code class="docutils literal notranslate"><span class="pre">f</span></code> from <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> to <code class="docutils literal notranslate"><span class="pre">V</span></code>, <code class="docutils literal notranslate"><span class="pre">Finsupp.linearCombination</span> <span class="pre">K</span> <span class="pre">f</span> <span class="pre">c</span></code> is the
sum over the support of <code class="docutils literal notranslate"><span class="pre">c</span></code> of the scalar multiplication <code class="docutils literal notranslate"><span class="pre">c</span> <span class="pre">&#8226;</span> <span class="pre">f</span></code>. In
particular, we can replace it by a sum over any finite set containing the
support of <code class="docutils literal notranslate"><span class="pre">c</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;&#8320;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c.support</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Finsupp.linearCombination</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finsupp.linearCombination_apply_of_mem_supported</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>One could also assume that <code class="docutils literal notranslate"><span class="pre">f</span></code> is finitely supported and still get a well defined sum.
But the choice made by <code class="docutils literal notranslate"><span class="pre">Finsupp.linearCombination</span></code> is the one relevant to our basis discussion since it allows
to state the generalization of <code class="docutils literal notranslate"><span class="pre">Basis.sum_repr</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finsupp.linearCombination</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="o">(</span><span class="n">B.repr</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">B.linearCombination_repr</span><span class="w"> </span><span class="n">v</span>
</pre></div>
</div>
<p>One could wonder why <code class="docutils literal notranslate"><span class="pre">K</span></code> is an explicit argument here, despite the fact it can be inferred from
the type of <code class="docutils literal notranslate"><span class="pre">c</span></code>. The point is that the partially applied <code class="docutils literal notranslate"><span class="pre">Finsupp.linearCombination</span> <span class="pre">K</span> <span class="pre">f</span></code>
is interesting in itself. It is not a bare function from <code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">&#8594;&#8320;</span> <span class="pre">K</span></code> to <code class="docutils literal notranslate"><span class="pre">V</span></code> but a
<code class="docutils literal notranslate"><span class="pre">K</span></code>-linear map.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="k">in</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Finsupp.linearCombination</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;&#8320;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
</pre></div>
</div>
<p>Returning to the mathematical discussion, it is important to understand that the
representation of vectors in a basis is less useful in formalized
mathematics than you may think.
Indeed it is very often more efficient to directly use more abstract properties of bases.
In particular the universal property of bases connecting them to other free objects in algebra
allows to construct linear maps by specifying the images of basis vectors.
This is <code class="docutils literal notranslate"><span class="pre">Basis.constr</span></code>. For any <code class="docutils literal notranslate"><span class="pre">K</span></code>-vector space <code class="docutils literal notranslate"><span class="pre">W</span></code>, our basis <code class="docutils literal notranslate"><span class="pre">B</span></code>
gives a linear isomorphism <code class="docutils literal notranslate"><span class="pre">Basis.constr</span> <span class="pre">B</span> <span class="pre">K</span></code> from <code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">&#8594;</span> <span class="pre">W</span></code> to <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">W</span></code>.
This isomorphism is characterized by the fact that it sends any function <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">:</span> <span class="pre">&#953;</span> <span class="pre">&#8594;</span> <span class="pre">W</span></code>
to a linear map sending the basis vector <code class="docutils literal notranslate"><span class="pre">B</span> <span class="pre">i</span></code> to <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">i</span></code>, for every <code class="docutils literal notranslate"><span class="pre">i</span> <span class="pre">:</span> <span class="pre">&#953;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">W</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">]</span>
<span class="w">         </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">u</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B.constr</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">))</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B.constr</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">B.constr</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="o">(</span><span class="n">B</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">B.constr_basis</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">i</span>
</pre></div>
</div>
<p>This property is indeed characteristic because linear maps are determined by their values
on bases:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">B</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">(</span><span class="n">B</span><span class="w"> </span><span class="n">i</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">B.ext</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>If we also have a basis <code class="docutils literal notranslate"><span class="pre">B'</span></code> on the target space then we can identify linear maps
with matrices. This identification is a <code class="docutils literal notranslate"><span class="pre">K</span></code>-linear isomorphism.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">B&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="o">]</span>

<span class="kn">open</span><span class="w"> </span><span class="n">LinearMap</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">Matrix</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>

<span class="kn">open</span><span class="w"> </span><span class="n">Matrix</span><span class="w"> </span><span class="c1">-- get access to the ``*&#7525;`` notation for multiplication between matrices and vectors.</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="bp">*&#7525;</span><span class="w"> </span><span class="o">(</span><span class="n">B.repr</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">B&#39;.repr</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">toMatrix_mulVec_repr</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span>


<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;&#39;&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">B&#39;&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;&#39;&#39;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;&#39;&#39;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#953;&#39;&#39;</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">B&#39;&#39;</span><span class="w"> </span><span class="bp">.</span><span class="n">id</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>As an exercise on this topic, we will prove part of the theorem which guarantees that
endomorphisms have a well-defined determinant.
Namely we want to prove that when two bases are indexed by the same type, the matrices
they attach to any endomorphism have the same determinant.
This would then need to be complemented using that bases all have isomorphic indexing types to
get the full result.</p>
<p>Of course Mathlib already knows this, and <code class="docutils literal notranslate"><span class="pre">simp</span></code> can close the goal immediately, so you
shouldn&#8217;t use it too soon, but rather use the provided lemmas.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Module</span><span class="w"> </span><span class="n">LinearMap</span><span class="w"> </span><span class="n">Matrix</span>

<span class="c1">-- Some lemmas coming from the fact that `LinearMap.toMatrix` is an algebra morphism.</span>
<span class="k">#check</span><span class="w"> </span><span class="n">toMatrix_comp</span>
<span class="k">#check</span><span class="w"> </span><span class="n">id_comp</span>
<span class="k">#check</span><span class="w"> </span><span class="n">comp_id</span>
<span class="k">#check</span><span class="w"> </span><span class="n">toMatrix_id</span>

<span class="c1">-- Some lemmas coming from the fact that ``Matrix.det`` is a multiplicative monoid morphism.</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Matrix.det_mul</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Matrix.det_one</span>

<span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">B&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">set</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">&#966;</span>
<span class="w">  </span><span class="n">set</span><span class="w"> </span><span class="n">M&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">&#966;</span>
<span class="w">  </span><span class="n">set</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span><span class="o">)</span><span class="w"> </span><span class="n">LinearMap.id</span>
<span class="w">  </span><span class="n">set</span><span class="w"> </span><span class="n">P&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">B</span><span class="o">)</span><span class="w"> </span><span class="n">LinearMap.id</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">end</span>
</pre></div>
</div>
</section>
<section id="dimension">
<h3><span class="section-number">10.4.3. </span>Dimension<a class="headerlink" href="#dimension" title="Link to this heading">&#61633;</a></h3>
<p>Returning to the case of a single vector space, bases are also useful to define the concept of
dimension.
Here again, there is the elementary case of finite-dimensional vector spaces.
For such spaces we expect a dimension which is a natural number.
This is <code class="docutils literal notranslate"><span class="pre">Module.finrank</span></code>. It takes the base field as an explicit argument
since a given abelian group can be a vector space over different fields.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span>

<span class="c1">-- `Fin n &#8594; K` is the archetypical space with dimension `n` over `K`.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Module.finrank_fin_fun</span><span class="w"> </span><span class="n">K</span>

<span class="c1">-- Seen as a vector space over itself, `&#8450;` has dimension one.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">&#8450;</span><span class="w"> </span><span class="n">&#8450;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Module.finrank_self</span><span class="w"> </span><span class="n">&#8450;</span>

<span class="c1">-- But as a real vector space it has dimension two.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">&#8450;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Complex.finrank_real_complex</span>
</pre></div>
</div>
<p>Note that <code class="docutils literal notranslate"><span class="pre">Module.finrank</span></code> is defined for any vector space. It returns
zero for infinite dimensional vector spaces, just as division by zero returns zero.</p>
<p>Of course many lemmas require a finite dimension assumption. This is the role of
the <code class="docutils literal notranslate"><span class="pre">FiniteDimensional</span></code> typeclass. For instance, think about how the next
example fails without this assumption.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">Nontrivial</span><span class="w"> </span><span class="n">V</span><span class="w">  </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Module.finrank_pos_iff</span>
</pre></div>
</div>
<p>In the above statement, <code class="docutils literal notranslate"><span class="pre">Nontrivial</span> <span class="pre">V</span></code> means <code class="docutils literal notranslate"><span class="pre">V</span></code> has at least two different elements.
Note that <code class="docutils literal notranslate"><span class="pre">Module.finrank_pos_iff</span></code> has no explicit argument.
This is fine when using it from left to right, but not when using it from right to left
because Lean has no way to guess <code class="docutils literal notranslate"><span class="pre">K</span></code> from the statement <code class="docutils literal notranslate"><span class="pre">Nontrivial</span> <span class="pre">V</span></code>.
In that case it is useful to use the name argument syntax, after checking that the lemma
is stated over a ring named <code class="docutils literal notranslate"><span class="pre">R</span></code>. So we can write:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nontrivial</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="o">(</span><span class="n">Module.finrank_pos_iff</span><span class="w"> </span><span class="o">(</span><span class="n">R</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">K</span><span class="o">))</span><span class="bp">.</span><span class="mi">1</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>The above spelling is strange because we already have <code class="docutils literal notranslate"><span class="pre">h</span></code> as an assumption, so we could
just as well give the full proof <code class="docutils literal notranslate"><span class="pre">Module.finrank_pos_iff.1</span> <span class="pre">h</span></code> but it
is good to know for more complicated cases.</p>
<p>By definition, <code class="docutils literal notranslate"><span class="pre">FiniteDimensional</span> <span class="pre">K</span> <span class="pre">V</span></code> can be read from any basis.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">B</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">Finite</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">FiniteDimensional.of_fintype_basis</span><span class="w"> </span><span class="n">B</span>

<span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finite</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">FiniteDimensional.fintypeBasisIndex</span><span class="w"> </span><span class="n">B</span><span class="o">)</span><span class="bp">.</span><span class="n">finite</span>
<span class="kd">end</span>
</pre></div>
</div>
<p>Using that the subtype corresponding to a linear subspace has a vector space structure,
we can talk about the dimension of a subspace.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span>

<span class="kn">open</span><span class="w"> </span><span class="n">Module</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span>
<span class="w">    </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Submodule.finrank_sup_add_finrank_inf_eq</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="n">F</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Submodule.finrank_le</span><span class="w"> </span><span class="n">E</span>
</pre></div>
</div>
<p>In the first statement above, the purpose of the type ascriptions is to make sure that
coercion to <code class="docutils literal notranslate"><span class="pre">Type*</span></code> does not trigger too early.</p>
<p>We are now ready for an exercise about <code class="docutils literal notranslate"><span class="pre">finrank</span></code> and subspaces.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Nontrivial</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">end</span>
</pre></div>
</div>
<p>Let us now move to the general case of dimension theory. In this case
<code class="docutils literal notranslate"><span class="pre">finrank</span></code> is useless, but we still have that, for any two bases of the same
vector space, there is a bijection between the types indexing those bases. So we
can still hope to define the rank as a cardinal, i.e. an element of the &#8220;quotient of
the collection of types under the existence of a bijection equivalence
relation&#8221;.</p>
<p>When discussing cardinal, it gets harder to ignore foundational issues around Russel&#8217;s paradox
like we do everywhere else in this book.
There is no type of all types because it would lead to logical inconsistencies.
This issue is solved by the hierarchy of universes that
we usually try to ignore.</p>
<p>Each type has a universe level, and those levels behave similarly to natural
numbers.&#8239;In particular there is zeroth level, and the corresponding universe
<code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">0</span></code> is simply denoted by <code class="docutils literal notranslate"><span class="pre">Type</span></code>. This universe is enough to hold
almost all of classical mathematics. For instance <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> have type <code class="docutils literal notranslate"><span class="pre">Type</span></code>.
Each level <code class="docutils literal notranslate"><span class="pre">u</span></code> has a successor denoted
by <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">+</span> <span class="pre">1</span></code>, and <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">u</span></code> has type <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">(u+1)</span></code>.</p>
<p>But universe levels are not natural numbers, they have a really different nature and don&#8217;t
have a type. In particular you cannot state in Lean something like <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">&#8800;</span> <span class="pre">u</span> <span class="pre">+</span> <span class="pre">1</span></code>.
There is simply no type where this would take place. Even stating
<code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">u</span> <span class="pre">&#8800;</span> <span class="pre">Type</span> <span class="pre">(u+1)</span></code> does not make any sense since <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">u</span></code> and <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">(u+1)</span></code>
have different types.</p>
<p>Whenever we write <code class="docutils literal notranslate"><span class="pre">Type*</span></code>, Lean inserts a universe level variable named <code class="docutils literal notranslate"><span class="pre">u_n</span></code> where <code class="docutils literal notranslate"><span class="pre">n</span></code> is a
number. This allows definitions and statements to live in all universes.</p>
<p>Given a universe level <code class="docutils literal notranslate"><span class="pre">u</span></code>, we can define an equivalence relation on <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">u</span></code> saying
two types <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#946;</span></code> are equivalent if there is a bijection between them.
The quotient type <code class="docutils literal notranslate"><span class="pre">Cardinal.{u}</span></code> lives in <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">(u+1)</span></code>. The curly braces
denote a universe variable. The image of <code class="docutils literal notranslate"><span class="pre">&#945;</span> <span class="pre">:</span> <span class="pre">Type</span> <span class="pre">u</span></code> in this quotient is
<code class="docutils literal notranslate"><span class="pre">Cardinal.mk</span> <span class="pre">&#945;</span> <span class="pre">:</span> <span class="pre">Cardinal.{u}</span></code>.</p>
<p>But we cannot directly compare cardinals in different universes. So technically we
cannot define the rank of a vector space <code class="docutils literal notranslate"><span class="pre">V</span></code> as the cardinal of all types indexing
a basis of <code class="docutils literal notranslate"><span class="pre">V</span></code>.
So instead it is defined as the supremum <code class="docutils literal notranslate"><span class="pre">Module.rank</span> <span class="pre">K</span> <span class="pre">V</span></code> of cardinals of
all linearly independent sets in <code class="docutils literal notranslate"><span class="pre">V</span></code>. If <code class="docutils literal notranslate"><span class="pre">V</span></code> has universe level <code class="docutils literal notranslate"><span class="pre">u</span></code> then
its rank has type <code class="docutils literal notranslate"><span class="pre">Cardinal.{u}</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="c1">-- Type u_2</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Module.rank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="c1">-- Cardinal.{u_2}</span>
</pre></div>
</div>
<p>One can still relate this definition to bases. Indeed there is also a commutative <code class="docutils literal notranslate"><span class="pre">max</span></code>
operation on universe levels, and given two universe levels <code class="docutils literal notranslate"><span class="pre">u</span></code> and <code class="docutils literal notranslate"><span class="pre">v</span></code>
there is an operation <code class="docutils literal notranslate"><span class="pre">Cardinal.lift.{u,</span> <span class="pre">v}</span> <span class="pre">:</span> <span class="pre">Cardinal.{v}</span> <span class="pre">&#8594;</span> <span class="pre">Cardinal.{max</span> <span class="pre">v</span> <span class="pre">u}</span></code>
that allows to put cardinals in a common universe and state the dimension theorem.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">universe</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="c1">-- `u` and `v` will denote universe levels</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="w"> </span><span class="n">u</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">B</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
<span class="w">         </span><span class="o">{</span><span class="n">&#953;&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="w"> </span><span class="n">v</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">B&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Cardinal.lift</span><span class="bp">.</span><span class="o">{</span><span class="n">v</span><span class="o">,</span><span class="w"> </span><span class="n">u</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="bp">.</span><span class="n">mk</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Cardinal.lift</span><span class="bp">.</span><span class="o">{</span><span class="n">u</span><span class="o">,</span><span class="w"> </span><span class="n">v</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="bp">.</span><span class="n">mk</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">mk_eq_mk_of_basis</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span>
</pre></div>
</div>
<p>We can relate the finite dimensional case to this discussion using the coercion
from natural numbers to finite cardinals (or more precisely the finite cardinals which live in <code class="docutils literal notranslate"><span class="pre">Cardinal.{v}</span></code> where <code class="docutils literal notranslate"><span class="pre">v</span></code> is the universe level of <code class="docutils literal notranslate"><span class="pre">V</span></code>).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Cardinal</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Module.rank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Module.finrank_eq_rank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span>
</pre></div>
</div>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C09_Groups_and_Rings.html" class="btn btn-neutral float-left" title="9. Groups and Rings" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C11_Topology.html" class="btn btn-neutral float-right" title="11. Topology" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>